\subsection{Introduction}
The idea behind forcing is to widen a given model of \( \mathsf{ZFC} \) to `add lots of reals'.
But if we work over \( \mathrm{V} \), we already have added all of the sets, so there is nothing left to add.
Instead, we will work over countable transitive set models of \( \mathsf{ZFC} \).
However, this means that we will not immediately get \( \Con(\mathsf{ZF}) \to \Con(\mathsf{ZFC} + \neg\mathsf{CH}) \).
We will then use the reflection theorem to obtain this result.

If \( M \) is such a countable transitive model, we want to add \( \omega_2^M \)-many reals to \( M \).
We will try to do this a `minimal way'; for example, we do not want to add any ordinals.
This gives us much more control over the model that we build.

Recall the argument that the sentence \( \varphi(x) \equiv \exists x.\, x^2 = 2 \) is independent of the axioms of fields: we began with a field in which the sentence failed, namely \( \mathbb Q \), and then extended it in a minimal way to \( \mathbb Q\qty[\sqrt{2}] \).
The model \( \mathbb Q\qty[\sqrt{2}] \) does not just contain \( \mathbb Q \cup \qty{\sqrt{2}} \), it also contains everything that can be built from \( \mathbb Q \) and \( \sqrt{2} \) using the axioms of fields.
The field \( \mathbb Q\qty[\sqrt{2}] \) is the minimal field extension of \( \mathbb Q \) satisfying \( \varphi \).

We may encounter some difficulties when adding arbitrary reals to our model.
Suppose that \( M \) is of the form \( \mathrm{L}_\gamma \), where \( \gamma \) is a countable ordinal.
Then \( \gamma \) can be coded as a subset \( c \) of \( \omega \), which can be viewed as a real.
If we added \( c \) to \( M \), we could decode it to form \( \gamma = \mathrm{Ord} \cap M \).
This would violate the principle of not adding any new ordinals.

Suppose we enumerate all formulas as \( \qty{\varphi_n \mid n \in \omega} \).
Let \( r = \qty{n \mid M \vDash \varphi_n} \).
If we added \( r \) to \( M \), we could then build a truth predicate for \( M \).
This would cause problems due to Tarski.

The main issues we must overcome are the following.
\begin{enumerate}
    \item We need a method to choose the \( \omega_2^M \)-many subsets of \( M \) to be added.
    \item Given these, we need to ensure that the extension satisfies \( \mathsf{ZFC} \).
    \item We must ensure that \( \omega_1^M \) and \( \omega_2^M \) are still cardinals in the extension.
\end{enumerate}
We will build these reals from within \( M \) itself.
Note that if \( r \) is a real, then each of its finite decimal approximations is already in \( M \).
The issue is that from within \( M \), we do not know what the real we want to add is.
So we may not know from within \( M \) which reals we will add.
Instead, we will add a \emph{generic} real.
To be generic, we will not specify any particular digits, but its decimal expansion will contain every finite sequence.
We will call a specification \emph{dense} if any finite approximation can be extended to one satisfying the specification.
For example, `beginning with a \( 7 \)' is not dense, but `containing the subsequence \( 746 \)' is dense.
It turns out that a real is generic precisely when it meets every dense specification.

Note that there are explicit, absolute bijections \( f : \mathcal P(\omega) \to \omega^\omega \), \( g : \omega^\omega \to 2^\omega \), \( h : 2^\omega \to \mathbb R \) and so on.
So if \( M \vDash \mathsf{ZFC} \), knowledge of \( \mathcal P^M(\omega) \) gives us \( (\omega^\omega)^M, (2^\omega)^M, \mathbb R^M \).
Because of this, by a `real' we mean either an element of \( \mathbb R \), a function \( \omega \to \omega \), a function \( \omega \to 2 \), or a subset of \( \omega \).
In formal arguments, reals will normally be either subsets of \( \omega \) or functions \( \omega \to 2 \).

The axiom of choice is not needed in the basic machinery of forcing, so we will work primarily over \( \mathsf{ZF} \) and state explicitly where choice is used.

\subsection{Forcing posets}
\begin{definition}
    A \emph{preorder} is a pair \( (\mathbb P, \leq) \) such that
    \begin{itemize}
        \item \( \mathbb P \) is nonempty;
        \item \( \leq \) is a binary relation on \( \mathbb P \);
        \item \( \leq \) is transitive, so \( p \leq q \) and \( q \leq r \) implies \( p \leq r \);
        \item \( \leq \) is reflexive, so \( p \leq p \).
    \end{itemize}
    A preorder is called a \emph{partial order} if \( \leq \) is antisymmetric, so \( p \leq q \) and \( q \leq p \) implies \( p = q \).
\end{definition}
\begin{definition}
    A \emph{forcing poset} is a triple \( (\mathbb P, \leq_{\mathbb P}, \Bbbone_{\mathbb P}) \), where \( (\mathbb P, \leq_{\mathbb P}) \) is a preorder and \( \Bbbone_{\mathbb P} \) is a maximal element.
    Elements of \( \mathbb P \) are called \emph{conditions}, and we say \( q \) is \emph{stronger} than \( p \) or an \emph{extension} of \( p \) if \( q \leq p \).
    We say that \( p, q \) are \emph{compatible}, written \( p \mathrel{\|}_{\mathbb P} q \), if there exists \( r \) such that \( r \leq_{\mathbb P} p, q \).
    Otherwise, we say they are \emph{incompatible}, written \( p \perp q \).
\end{definition}
\begin{remark}
    In some texts, the partial order is reversed.
    This is called \emph{Jerusalem notation}.
\end{remark}
The notation \( \mathbb P \in M \) abbreviates \( (\mathbb P, \leq_{\mathbb P}, \Bbbone_{\mathbb P}) \in M \).
Note that by transitivity if \( \mathbb P \) is an element of \( M \), then \( \Bbbone_{\mathbb P} \in M \), but we do not necessarily have \( {\leq_{\mathbb P}} \in M \).
\begin{definition}
    A preorder is \emph{separative} if whenever \( p \neq q \), exactly one of the following two cases holds:
    \begin{enumerate}
        \item \( q \leq p \) and \( p \nleq q \); or
        \item there exists \( r \leq q \) such that \( r \perp p \).
    \end{enumerate}
\end{definition}
\begin{proposition}
    If \( (\mathbb P, \leq) \) is a separative preorder, it is a partial order.
\end{proposition}
\begin{proposition}
    Suppose that \( (\mathbb P, \leq) \) is a preorder.
    Define \( p \sim q \) by
    \[ p \sim q \leftrightarrow \forall r \in P.\, (r \mathrel\| p \leftrightarrow r \mathrel\| q) \]
    Then there is a separative preorder on \( \faktor{\mathbb P}{\sim} \) such that
    \[ [p] \perp [q] \leftrightarrow p \perp q \]
    and if \( \mathbb P \) has a maximal element, so does \( \faktor{\mathbb P}{\sim} \).
\end{proposition}
\begin{example}
    For sets \( I, J \), we let \( \Fn(I, J) \) denote the set of all finite partial functions from \( I \) to \( J \).
    \[ \Fn(I, J) = \qty{p \mid \abs{p} < \omega \wedge p \text{ is a function} \wedge \dom p \subseteq I \wedge \ran p \subseteq J} \]
    We let \( \leq \) be the reverse inclusion on \( \Fn(I, J) \), so \( q \leq p \) if and only if \( q \supseteq p \).
    The maximal element \( \Bbbone \) is the empty set.
    Then \( (\Fn(I, J), \leq, \varnothing) \) is a forcing poset, and moreover, the preorder is separative.
\end{example}
\begin{remark}
    When \( \alpha \) is an ordinal, the forcing poset \( \Fn(\alpha \times \omega, 2) \) is often written \( \operatorname{Add}(\omega, \alpha) \), denoting the idea that we are adding \( \alpha \)-many subsets of \( \omega \).
\end{remark}

\subsection{Chains and \texorpdfstring{\( \Delta \)}{Δ}-systems}
\begin{definition}
    Let \( \mathbb P \) be a forcing poset.
    \begin{enumerate}
        \item A \emph{chain} is a subset \( C \subseteq \mathbb P \) such that for every \( p, q \in C \), either \( p \leq q \) or \( q \leq p \).
        \item An \emph{antichain} is a subset \( A \subseteq \mathbb P \) such that for every \( p, q \in A \), either \( p = q \) or \( p \perp q \).
        An antichain is \emph{maximal} if it is not strictly contained in any other antichain.
        \item We say that \( \mathbb P \) has the \emph{countable chain condition} if every antichain is countable.
    \end{enumerate}
\end{definition}
\begin{example}
    \begin{enumerate}
        \item Consider the tree \( \Fn(\omega, 2) \).
        A chain is a branch through the tree, and an antichain is a collection of points on different branches.
        \item The set of functions \( \qty{\qty{\langle 0, 0 \rangle, \langle 1, n \rangle} \mid n \in \omega} \) forms an antichain of length \( \omega \) in \( \Fn(I, \omega) \) if \( \qty{0,1} \subseteq I \).
    \end{enumerate}
\end{example}
\begin{definition}
    A family of sets \( \mathcal A \) forms a \emph{\( \Delta \)-system with root \( R \)} when \( X \cap Y = R \) for all \( X \neq Y \) in \( \mathcal A \).
\end{definition}
\begin{example}
    If \( R = \varnothing \), then \( \mathcal A \) is a family of pairwise disjoint sets.
\end{example}
\begin{definition}
    Let \( A \) be a set and \( \theta \) a cardinal.
    Then we write \( [A]^\theta \) for the set of subsets of \( A \) of size \( \theta \).
    \[ [A]^\theta = \qty{x \subseteq A \mid \abs{x} = \theta} \]
    We write \( [A]^{<\theta} \) for the set of subsets of \( A \) of size strictly less than \( \theta \).
    \[ [A]^{<\theta} = \qty{x \subseteq A \mid \abs{x} < \theta} \]
    Similarly, \( [A]^{\leq\theta} = [A]^\theta \cup [A]^{<\theta} \).
\end{definition}
Recall that for regular cardinals \( \kappa \), if \( \mathcal F \) is a family of sets of size less than \( \kappa \) and each element of \( \mathcal F \) has size less than \( \kappa \), then \( \bigcup \mathcal F \) has size less than \( \kappa \).
\begin{lemma}[\( \Delta \)-system lemma]
    (\( \mathsf{ZFC} \))
    Let \( \kappa \) be an uncountable regular cardinal, and let \( \mathcal A \) be a family of finite sets with \( \abs{\mathcal A} = \kappa \).
    Then there exists \( \mathcal B \in [\mathcal A]^\kappa \) that forms a \( \Delta \)-system.
\end{lemma}
\begin{proof}
    To begin, we construct \( \mathcal C \in [\mathcal A]^\kappa \) such that all elements of \( \mathcal C \) have the same cardinality.
    By assumption, each element of \( \mathcal A \) is finite, and so we can define \( Y_n = \qty{X \in \mathcal A \mid \abs{X} = n} \), and suppose each of the \( Y_n \) had size less than \( \kappa \).
    Then \( \abs{\mathcal A} = \abs{\bigcup Y_n} < \kappa \), giving a contradiction.

    Fix \( n \in \omega \) such that \( \mathcal C = Y_n \) has size \( \kappa \).
    We show by induction on \( n \) that if \( \mathcal C = \qty{X \in \mathcal A \mid \abs{X} = n} \), then there is \( \mathcal B \subseteq \mathcal C \) of size \( \kappa \) that forms a \( \Delta \)-system.
    If \( n = 1 \), we have a collection of pairwise disjoint singletons, so \( \mathcal C \) is already a \( \Delta \)-system with root \( \varnothing \) as required.
    Now suppose \( n > 1 \) and the claim holds for \( n - 1 \).
    For each \( p \in \bigcup \mathcal C \), let \( C_p = \qty{X \in \mathcal C \mid p \in X} \).
    There are two cases to consider.

    Suppose \( \abs{C_p} = \kappa \) for some \( p \in \bigcup \mathcal C \).
    Then for such a \( p \), we set \( \mathcal D = \qty{X \setminus \qty{p} \mid X \in C_p} \).
    This set has size \( \kappa \), and each element of \( \mathcal D \) has size \( n - 1 \).
    By the inductive hypothesis, we can find some \( \mathcal E \in [\mathcal D]^\kappa \) such that \( \mathcal E \) forms a \( \Delta \)-system with root \( R \).
    Then \( \qty{Y \cup \qty{b} \mid Y \in \mathcal E} \) is a \( \Delta \)-system with root \( R \cup \qty{p} \).

    Now suppose all of the \( C_p \) have size less than \( \kappa \).
    Then as \( \kappa \) is regular, for any set \( S \) of size less than \( \kappa \),
    \[ \qty{X \in \mathcal C \mid X \cap S \neq \varnothing} = \bigcup_{p \in S} C_p \]
    has size less than \( \kappa \).
    Therefore, there exists some \( X \in \mathcal C \) such that \( X \cap S = \varnothing \).
    We recursively choose \( X_\alpha \in \mathcal C \) for each \( \alpha < \kappa \) such that \( X_\alpha \cap \bigcup_{\beta < \alpha} X_\beta = \varnothing \).
    Then \( {X_\alpha \mid \alpha < \kappa} \in [\mathcal C]^\kappa \) is a \( \Delta \)-system with empty root.
\end{proof}
We can show that assumptions in the above lemma were required.
\begin{proposition}
    Suppose \( \kappa \) is \( \omega \) or singular.
    Then there exists a family \( \mathcal A \) of finite sets with \( \abs{\mathcal A} = \kappa \) but no \( \mathcal B \in [\mathcal A]^\kappa \) forms a \( \Delta \)-system.
\end{proposition}
\begin{lemma}
    (\( \mathsf{ZFC} \))
    \( \Fn(I, J) \) has the countable chain condition if and only if \( I \) is empty or \( J \) is countable.
\end{lemma}
\begin{proof}
    First, we observe that if \( I \) or \( J \) are empty, then \( \Fn(I, J) \) is empty and so trivially has the countable chain condition.
    Now let us assume that both \( I \) and \( J \) are nonempty.

    Suppose that \( J \) is uncountable.
    Then for any \( i \in I \), the set
    \[ \qty{\qty{\langle i, j \rangle} \mid j \in J} \]
    is an uncountable antichain.

    Now suppose \( J \) is countable, and let \( \qty{p_\alpha \mid \alpha \in \omega_1} \) be a collection of distinct elements of \( \Fn(I, J) \).
    Let \( \mathcal A = \qty{\dom p_\alpha \mid \alpha \in \omega_1} \), which is a collection of \( \omega_1 \)-many finite sets.
    By the \( \Delta \)-system lemma, we can find an uncountable subset \( \mathcal B \subseteq \mathcal A \) with a root \( R \subseteq I \).
    By definition, \( R \subseteq \dom(p_\alpha) \) for all \( \dom p_\alpha \in \mathcal B \), the root \( R \) must be finite.
    Since \( J \) is countable, there are only countably many functions \( R \to J \).
    Therefore, as \( \mathcal B \) is uncountable, there are \( \alpha \neq \beta \) such that \( \dom p_\alpha \) and \( \dom p_\beta \) are both in \( \mathcal B \) and \( \eval{p_\alpha}_R = \eval{p_\beta}_R \).
    But then since \( R \) is a root, \( \dom p_\alpha \cap \dom p_\beta = R \), so \( p_\alpha \mathrel\| p_\beta \), witnessed by their union \( p_\alpha \cup p_\beta \).
    So the \( \qty{p_\alpha \mid \alpha \in \omega_1} \) cannot form an antichain.
\end{proof}

\subsection{Dense sets and genericity}
\begin{definition}
    Let \( \mathbb P \) be a forcing poset.
    \begin{enumerate}
        \item \( D \subseteq \mathbb P \) is \emph{dense} if for all \( p \in \mathbb P \) there exists \( q \in D \) such that \( q \leq p \).
        \item \( D \subseteq \mathbb P \) is \emph{open} if for all \( p \in D \) and \( q \in \mathbb P \), if \( q \leq p \) then \( q \in D \).
    \end{enumerate}
\end{definition}
A set of conditions is dense if every condition can be extended to one in that set, and a set is open if it is closed under strengthening conditions.
\begin{example}
    Let \( I \) be infinite and \( J \) nonempty.
    Then for all \( i \in I \) and \( j \in J \), the following are dense.
    \begin{enumerate}
        \item \( D_i = \qty{q \in \Fn(I, J) \mid i \in \dom q} \);
        \item \( R_j = \qty{q \in \Fn(I, J) \mid j \in \ran q} \).
    \end{enumerate}
\end{example}
\begin{definition}
    A subset \( G \) of a forcing poset \( \mathbb P \) is a \emph{filter} if
    \begin{enumerate}
        \item \( \Bbbone \in G \);
        \item for all \( p, q \in G \) there is \( r \in G \) such that \( r \leq p \) and \( r \leq q \);
        \item for all \( p, q \in G \), if \( q \leq p \) and \( q \in G \) then \( p \in G \).
    \end{enumerate}
    A filter \( G \) is \emph{\( \mathbb P \)-generic over \( M \)} if \( G \cap D \) is nonempty for every \( \mathbb P \)-dense subset \( D \in M \).
\end{definition}
\begin{lemma}[generic filter existence lemma]
    Let \( M \) be an arbitrary countable set, and let \( \mathbb P \in M \) be a forcing poset.
    Then for any condition \( p \in \mathbb P \), there is a filter \( G \subseteq \mathbb P \) containing \( p \) which is \( \mathbb P \)-generic over \( M \).
\end{lemma}
\begin{proof}
    Let \( (D_n)_{n \in \omega} \) enumerate all dense subsets of \( \mathbb P \) which lie in \( M \).
    We inductively define \( X \subseteq \mathbb P \) by \( X = \qty{q_n \mid n \in \omega} \) as follows.
    Let \( q_0 = p \), and given \( q_n \), we choose \( q_{n+1} \in D_n \) such that \( q_{n+1} \leq q_n \).
    Finally, let \( G = \qty{r \in \mathbb P \mid \exists n.\, q_n \leq r} \).
    Then \( G \) is a filter as the \( q_n \) form a chain, and it is clearly generic.
\end{proof}
\begin{definition}
    A condition \( p \in \mathbb P \) is \emph{minimal} if whenever \( q \leq p \), we have \( q = p \).
\end{definition}
\begin{lemma}
    Let \( M \) be a countable transitive model of \( \mathsf{ZF} \), and let \( \mathbb P \in M \) be a separative partial order.
    Then either \( \mathbb P \) has a minimal element, or for every filter \( G \) which is \( \mathbb P \)-generic over \( M \), we have \( G \notin M \).
\end{lemma}
\begin{proof}
    Suppose \( \mathbb P \) has no minimal element.
    Let \( G \) be a \( \mathbb P \)-generic filter over \( M \).
    We show that if \( F \subseteq \mathbb P \) is a filter in \( M \), then the set \( D_F = \mathbb P \setminus F \in M \) is a dense set.
    Then \( G \cap D_F \) is nonempty for all filters \( F \), so \( G \) cannot be equal to any filter \( F \in M \).

    Fix \( p \in \mathbb P \).
    If \( p \notin F \), then \( p \in D_F \) as required.
    Otherwise, suppose \( p \in F \).
    As \( p \) is not minimal, we can fix some \( q \in F \) with \( q < p \).
    Then \( p \nleq q \), so by separativity, there is \( r \leq p \) such that \( r \perp q \).
    But all conditions in \( F \) are compatible, so one of \( r \) and \( q \) is not in \( F \).
\end{proof}
\begin{proposition}
    For sets \( I, J \) such that \( \abs{I} \geq \omega \) and \( \abs{J} \geq 2 \), the forcing poset \( \Fn(I, J) \) is a separative partial order without a minimal element.
\end{proposition}
\begin{proposition}
    (\( \mathsf{ZFC} \))
    Let \( \mathbb P \in M \) be a forcing poset, and let \( G \subseteq \mathbb P \).
    Then the following are equivalent.
    \begin{enumerate}
        \item \( G \) is \( \mathbb P \)-generic over \( M \), that is, for all dense sets \( D \in M \), we have \( G \cap D \neq \varnothing \);
        \item for all \( p \in G \) and \( D \in M \), if \( D \) is dense below \( p \) in \( \mathbb P \), then \( G \cap D \neq \varnothing \);
        \item for all open dense sets \( D \in M \), we have \( G \cap D \neq \varnothing \);
        \item for all \( D \in M \) that are maximal antichains in \( \mathbb P \), we have \( G \cap D \neq \varnothing \).
    \end{enumerate}
\end{proposition}

\subsection{Names}
\begin{definition}
    Let \( \mathbb P \) be a forcing poset.
    We define the class of \emph{\( \mathbb P \)-names} \( M^{\mathbb P} \) recursively as follows.
    \begin{enumerate}
        \item \( M_0^{\mathbb P} = \varnothing \);
        \item \( M_{\alpha + 1}^{\mathbb P} = \mathcal P^M(\mathbb P \times M_\alpha^{\mathbb P}) \);
        \item at limit stages \( \lambda \), \( M_\lambda^{\mathbb P} = \bigcup_{\alpha < \lambda} M_\alpha^{\mathbb P} \);
        \item \( M^{\mathbb P} = \bigcup_{\alpha \in \mathrm{Ord}} M_\alpha^{\mathbb P} \).
    \end{enumerate}
\end{definition}
Being a \( \mathbb P \)-name is absolute for transitive models.
\( \mathbb P \)-names are denoted with overdots, such as in \( \dot x \).
\begin{definition}
    The \emph{range} of a \( \mathbb P \)-name \( \dot x \) is
    \[ \ran(\dot x) = \qty{\dot y \mid \exists p \in \mathbb P.\, \langle p, \dot y \rangle \in \dot x} \]
\end{definition}
\begin{remark}
    Alternatively, by transfinite recursion on rank, we could define the class of \( \mathbb P \)-names over \( \mathrm{V} \) in the following way.
    If \( \rank x = \alpha \), then \( x \) is a \( \mathbb P \)-name if and only if it is a relation such that for all \( \langle p, \dot y \rangle \in x \), we have \( p \in \mathbb P \) and \( \dot y \) is a \( \mathbb P \)-name in \( \mathrm{V}_\alpha \).
    Finally, \( M^{\mathbb P} = \mathrm{V}^{\mathbb P} \cap M \).
\end{remark}
\begin{definition}
    The \emph{\( \mathbb P \)-rank} of a name \( \dot x \), written \( \rank_{\mathbb P} \dot x \), is the least \( \alpha \) such that \( \dot x \subseteq \mathbb P \times M_\alpha^{\mathbb P} \).
\end{definition}
\begin{definition}
    Let \( \dot x \) be a \( \mathbb P \)-name and \( G \) be an arbitrary subset of \( \mathbb P \).
    We define the \emph{interpretation of \( \dot x \) by \( G \)} recursively by
    \[ \dot x^G = \qty{\dot y^G \mid \exists p \in G.\, \langle p, \dot y \rangle \in \dot x} \]
\end{definition}
\begin{definition}
    The \emph{forcing extension of \( M \) by \( G \)}, written \( M[G] \), is
    \[ M[G] = \qty{\dot x^G \mid \dot x \in M^{\mathbb P}} \]
\end{definition}
\begin{example}
    \begin{enumerate}
        \item If \( \varnothing \in M \), then \( \varnothing^G = \varnothing \).
        \item Let
        \[ \dot x = \qty{\langle p, \varnothing \rangle, \langle r, \qty{\langle q, \varnothing \rangle} \rangle} \]
        If \( p, q, r \in G \), then
        \begin{align*}
            \dot x^G &= \qty{(\langle p, \varnothing \rangle)^G, \qty(\langle r, \qty{\langle q, \varnothing \rangle} \rangle)^G} \\
            &= \qty{\varnothing, \qty{(\langle q, \varnothing \rangle)^G}} \\
            &= \qty{\varnothing, \qty{\varnothing}}
        \end{align*}
        If \( p, r \notin G \), then
        \[ \dot x^G = \varnothing \]
        If \( r \in G \) but \( p, q \notin G \), then
        \[ \dot x^G = \qty{(\langle q, \varnothing \rangle)^G} = \qty{\varnothing} \]
        Finally, if \( p \in G \) but \( r \notin G \), then
        \[ \dot x^G = \qty{\varnothing} \]
    \end{enumerate}
\end{example}
We aim to show the following major theorem.
\begin{theorem}[generic model theorem]
    Let \( M \) be a countable transitive model of \( \mathsf{ZF} \), let \( \mathbb P \) be a forcing poset, and let \( G \) be a \( \mathbb P \)-generic filter.
    Then
    \begin{enumerate}
        \item \( M[G] \) is a transitive set;
        \item \( \abs{M[G]} = \aleph_0 \);
        \item \( M[G] \vDash \mathsf{ZF} \), and if \( M \vDash \mathsf{AC} \) then \( M[G] \vDash \mathsf{AC} \);
        \item \( \mathrm{Ord}^M = \mathrm{Ord}^{M[G]} \);
        \item \( M \subseteq M[G] \);
        \item \( M[G] \) is the smallest countable transitive model of \( \mathsf{ZF} \) such that \( M \subseteq M[G] \) and \( G \) is a set in \( M[G] \).
    \end{enumerate}
\end{theorem}
Countability is only needed to show the existence of a generic filter, so parts (i) and (iii)--(vi) of this theorem hold without this assumption.

\subsection{Canonical names}
We can prove some parts of the generic model theorem by introducing the notion of \emph{canonical names}.
\begin{definition}
    Given a forcing poset \( (\mathbb P, \leq, \Bbbone) \) and a set \( x \in M \), we define the \emph{canonical} name of \( x \) by
    \[ \check x = \qty{\langle \Bbbone, \check y \rangle \mid y \in x} \]
\end{definition}
The symbol \( \check x \) is pronounced \emph{\( x \)-check}.
\begin{lemma}
    If \( M \) is a transitive model of \( \mathsf{ZF} \), \( \mathbb P \in M \), and \( \Bbbone \in G \subseteq \mathbb P \), then
    \begin{itemize}
        \item for all \( x \in M \), \( \check x \in M^{\mathbb P} \) and \( \check x^G = x \);
        \item \( M \subseteq M[G] \);
        \item \( M[G] \) is transitive.
    \end{itemize}
\end{lemma}
\begin{proof}
    \emph{Part (i).}
    We show \( \check x \in M^{\mathbb P} \) by induction, using the definition of \( \mathbb P \)-names by transfinite recursion.
    Hence
    \[ \check x^G = \qty{\check y^G \mid y \in x} = \qty{y \mid y \in x} = x \]
    Part (ii) follows directly from part (i).

    \emph{Part (iii).}
    Suppose that \( x \in y \) and \( y \in M[G] \).
    By definition, \( y = \dot y^G \) for some \( \mathbb P \)-name \( \dot y \).
    By construction, any element of \( y \) is of the form \( \dot z^G \), so in particular, \( x = \dot x^G \) for some \( \mathbb P \)-name \( \dot x \in M^{\mathbb P} \).
\end{proof}
\begin{remark}
    Even if \( G \notin M \), we can still define a name for \( G \) in \( M \).
    From this, it follows that if \( G \notin M \), then \( M[G] \neq M \).
\end{remark}
\begin{proposition}
    Let
    \[ \dot G = \qty{\langle p, \check p \rangle \mid p \in \mathbb P} \]
    Then \( \dot G^G = G \).
\end{proposition}
\begin{proof}
    \[ \dot G^G = \qty{\check p^G \mid p \in G} = \qty{p \mid p \in G} = G \]
\end{proof}

\subsection{???}
We can define unordered and ordered pairs of names, with sensible interpretations.
\begin{definition}
    Given \( \mathbb P \)-names \( \dot x, \dot y \), let
    \[ \operatorname{up}(\dot x, \dot y) = \qty{\langle \Bbbone, \dot x \rangle, \langle \Bbbone, \dot y \rangle} \]
    and
    \[ \operatorname{op}(\dot x, \dot y) = \operatorname{up}(\operatorname{up}(\dot x, \dot x), \operatorname{up}(\dot x, \dot y)) \]
\end{definition}
\begin{proposition}
    For \( \dot x, \dot y \in M^{\mathbb P} \) and \( \Bbbone \in G \subseteq \mathbb P \),
    \[ (\operatorname{up}(\dot x, \dot y))^G = \qty{\dot x^G, \dot y^G} \]
    and
    \[ (\operatorname{op}(\dot x, \dot y))^G = \langle \dot x^G, \dot y^G \rangle \]
\end{proposition}
\begin{lemma}
    Suppose \( M \) is a transitive model of \( \mathsf{ZF} \) and \( \mathbb P \in M \) is a forcing poset.
    If \( \Bbbone \in G \subseteq \mathbb P \), then \( M[G] \) is a transitive model of extensionality, empty set, foundation, and pairing.
\end{lemma}
\begin{lemma}
    Suppose that \( M \) is a transitive model of \( \mathsf{ZF} \) and \( \mathbb P \in M \) is a forcing poset.
    Let \( G \subseteq \mathbb P \) be such that \( \Bbbone \in G \).
    Then
    \begin{enumerate}
        \item \( \rank (\dot x^G) \leq \rank \dot x \) for all \( \dot x \in M^{\mathbb P} \);
        \item \( \mathrm{Ord}^M = \mathrm{Ord}^{M[G]} \);
        \item \( \abs{M[G]} = \abs{M} \).
    \end{enumerate}
\end{lemma}
\begin{proof}
    \emph{Part (i).}
    We show this result by induction on \( x \).
    \( \varnothing^G = \varnothing \), and both have rank \( 0 \).
    We have
    \begin{align*}
        \rank(\dot x^G) &= \sup\qty{\rank u + 1 \mid u \in \dot x^G} \\
        &\leq \sup\qty{\rank(\dot y^G) + 1 \mid \dot y \in \ran \dot x} \\
        &\leq \sup\qty{\rank \dot y + 1 \mid \dot y \in \ran \dot x} \\
        &\leq \sup\qty{\rank u + 1 \mid u \in \dot x} \\
        &\leq \rank \dot x
    \end{align*}

    \emph{Part (ii).}
    Since \( M \subseteq M[G] \) and being an ordinal is absolute, \( \mathrm{Ord}^M \subseteq \mathrm{Ord}^{M[G]} \).
    For the reverse inclusion, suppose \( \alpha \in M[G] \) is an ordinal, and fix a name \( \dot x \in M^{\mathbb P} \) such that \( \alpha = \dot x^G \).
    Then \( \alpha \) is an ordinal in the universe, so
    \[ \alpha = \rank \alpha \leq \rank \dot x \]
    so since \( M \) is transitive, \( \alpha \in \mathrm{Ord}^M \).

    \emph{Part (iii).}
    Since any element of \( M[G] \) is of the form \( \dot x^G \) for some \( \dot x \in M^{\mathbb P} \subseteq M \subseteq M[G] \), we must have
    \[ \abs{M[G]} \leq \abs{M^{\mathbb P}} \leq \abs{M} \leq \abs{M[G]} \]
    so the inequalities must be equalities.
\end{proof}
\begin{corollary}
    \( M[G] \) satisfies the axiom of infinity.
\end{corollary}
\begin{proof}
    \( \omega \in \mathrm{Ord}^M \) so \( \omega \in \mathrm{Ord}^{M[G]} \subseteq M[G] \).
\end{proof}
\begin{lemma}
    Suppose \( M \) is a transitive model of \( \mathsf{ZF} \), \( \mathbb P \in M \) is a forcing poset, and \( G \subseteq \mathbb P \) is such that \( \Bbbone \in G \).
    Then if \( N \) is another transitive model of \( \mathsf{ZF} \) with \( M \subseteq N \) a definable class in \( N \) and \( G \in N \), then \( M[G] \subseteq N \).
\end{lemma}
\begin{proof}
    We carry out the construction of \( M[G] \) in \( N \).
    Namely, we will show that for all \( \mathbb P \)-names \( \dot x \), we have \( \dot x^G \in N \), from which it follows that \( M[G] \subseteq N \).
    We proceed by induction on \( x \).
    As the axiom of empty set holds in \( N \) and it is a transitive set, \( \varnothing^G = \varnothing \in N \).
    Moreover, since
    \[ M^{\mathbb P} = \mathrm{V}^{\mathbb P} \cap M \subseteq \mathrm{V}^{\mathbb P} \cap N = N^{\mathbb P} \]
    if \( \dot x \) is a \( \mathbb P \)-name of \( M \), it must be a \( \mathbb P \)-name of \( M \).
    In particular, \( x \in N \).
    Now, suppose that for every \( \langle p, \dot y \rangle \in \dot x \), we have \( \dot y^G \in N \).
    Then
    \begin{align*}
        (\dot x^G)^N &= \qty{\dot y^G \mid \exists p \in G.\, \langle p, \dot y \rangle \in \dot x}^N \\
        &= \qty{(\dot y^G)^N \mid (\exists p \in G.\, \langle p, \dot y \rangle \in \dot x)^N} \\
        &= \qty{\dot y^G \mid \exists p \in G.\, \langle p, \dot y \rangle \in \dot x} \\
        &= \dot x^G
    \end{align*}
    Thus \( \dot x^G \in N \) as required.
\end{proof}
To prove the generic model theorem, it now suffices to prove the remaining axioms of \( \mathsf{ZF} \), which are union, power set, replacement, and separation.
We can prove the axiom of union now.
\begin{lemma}
    Suppose \( M \) is a transitive model of \( \mathsf{ZF} \), \( \mathbb P \in M \) is a forcing poset, and \( G \subseteq \mathbb P \) is such that \( \Bbbone \in G \).
    Additionally, suppose that \( G \) is a filter.
    Then \( M[G] \) satisfies the axiom of union.
\end{lemma}
\begin{proof}
    It suffices to prove that for all \( a \in M[G] \), there is some \( b \in M[G] \) such that \( \bigcup a = b \).
    Fix \( \dot a \in M^{\mathbb P} \) such that \( \dot a^G = a \), and let \( \dot b \) be the following name.
    \[ \dot b = \qty{\langle p, \dot z \rangle \mid \exists \langle q, \dot y \rangle \in \dot a.\, \exists r \in \mathbb P.\, \langle r, \dot z \rangle \in \dot y \wedge p \leq r, q} \]
    Observe that \( \dot b \) is a \( \mathbb P \)-name in \( M \): since \( \dot a \) is a \( \mathbb P \)-name, any \( \dot y \in \ran \dot a \) is a \( \mathbb P \)-name, so \( \dot b \) consists of pairs \( \langle p, \dot z \rangle \) where \( p \in \mathbb P \) and \( \dot z \in \ran \dot y \) for some \( \dot y \in \ran \dot a \).
    Thus \( \dot z \) is a \( \mathbb P \)-name in \( \mathrm{V} \).
    Moreover \( \dot b \in M \) since \( \dot b \in \mathbb P \times \operatorname{tcl}(\dot a) \).

    We claim that \( \bigcup a \subseteq \dot b^G \).
    Let \( w \in \bigcup a \), so \( w \in v \) for some \( v \in a \).
    Since \( M[G] \) is transitive, we can fix names \( \dot y, \dot z \) and conditions \( q, r \in G \) such that
    \[ \dot y^G = v;\quad \dot z^G = w;\quad \langle q, \dot y \rangle \in \dot a;\quad \langle r, \dot z \rangle \in \dot y \]
    As \( G \) is a filter, by directedness there is a condition \( p \leq q, r \) in \( G \).
    Then, by definition, \( \langle p, \dot z \rangle \in \dot b \), and \( w = \dot z^G \in \dot b^G \).

    For the converse, we claim that \( \dot b^G \subseteq \bigcup a \).
    Let \( \langle p, \dot z \rangle \in \dot b^G \), so \( p \in G \) and \( \dot z^G = c \).
    By definition, we can fix \( \langle q, \dot y \rangle \in \dot a \) and \( r \in \mathbb P \) such that \( \langle r, \dot z \rangle \in \dot y \) and \( p \leq q, r \).
    Using the fact that \( G \) is a filter, we must have \( q, r \in G \).
    Hence \( \dot z^G \in \dot y^G \) and \( \dot y^G \in \dot a^G \), so \( c \in \dot y^G \) for some \( \dot y^G \in a \).
\end{proof}
\begin{example}[motivation for genericity]
    Note that \( \mathbb P, G \in M[G] \).
    If \( M[G] \) models any reasonable theory, we should have \( \mathbb P \setminus G \in M[G] \).
    We will try to build a name for \( \mathbb P \setminus G \).
    A natural name to consider is
    \[ \dot c = \qty{\langle q, \dot p \rangle \mid p, q \in \mathbb P, p \perp q} \]
    Then
    \[ \dot c^G = \qty{p \mid \exists q \in G.\, p \perp q} \]
    If \( G \) is a filter, its elements are pairwise compatible, so \( G \cap \dot c^G = \varnothing \).
    But we still need to show that \( G \cup \dot c^G = \mathbb P \).
    For each condition \( p \), set
    \[ D_p = \qty{q \in \mathbb P \mid p \perp q \vee q \leq p} \]
    It is easy to check that \( D_p \in M \) is dense.
    Now, if \( G \) is \( \mathbb P \)-generic, we could fix some \( q \in G \cap D_p \) for any given \( p \).
    Then if \( p \perp q \), by definition \( p \in \dot c^G \), and if \( q \leq p \), then \( p \in G \) by upwards closure.
    From this, it follows that \( G \cup \dot c^G = \mathbb P \).
\end{example}
In fact, we have the following.
\begin{proposition}
    Let \( M \) be a countable transitive model of \( \mathsf{ZF} \).
    Then there exists a forcing poset \( \mathbb P \in M \) and a (non-generic) filter \( G \subseteq \mathbb P \) such that \( \mathbb P \setminus G \notin M[G] \).
\end{proposition}

\subsection{The forcing relation}
To show separation, we need to show that if \( \varphi(x, y) \) is a formula and \( \dot a, \dot b \) are \( \mathbb P \)-names, then
\[ C = \qty{\dot z \in \dot a^G \mid (\varphi(\dot z^G, \dot b^G))^{M[G]}} \in M[G] \]
This is unclear, even for simple formulas such as \( \varphi(x, y) \equiv x \notin y \).
We will build a way to formally reason about \( M[G] \) from within \( M \), without having to rely on \( G \).
To do this, we will define a relation \( p \Vdash \varphi \) between conditions \( p \in \mathbb P \) and names in \( \mathrm{V}^{\mathbb P} \).
Its relativisation \( (p \Vdash \varphi)^M \) will provide a way to work in \( M \).
Our aim is to define \( \Vdash \) such that \( p \Vdash \varphi(\dot u) \) if and only if for every generic subset \( G \subseteq \mathbb P \) with \( p \in G \), we have \( M[G] \vDash \varphi(\dot u^G) \).

Naively, we might say that if \( \langle p, \dot x \rangle \in \dot y \) then \( p \Vdash \dot x \in \dot y \).
The converse cannot be made to hold.
Consider \( \dot x = \qty{\langle p, \varnothing \rangle} \) where \( p \neq \Bbbone \).
Then \( p \Vdash \varnothing \in \dot x \).
Suppose \( q \perp p \), then we have \( q \Vdash \dot x = \varnothing \).
Therefore, we should have \( q \Vdash \dot x \in \check 1 \).
If we enforce the converse above, we would have \( \langle q, \dot x \rangle \in \check 1 \), which is incorrect since \( \check 1 = \qty{\langle \Bbbone, \varnothing \rangle} \).
Instead, we will define the forcing relation in terms of dense sets, leveraging the fact that generics meet all dense sets.
\begin{definition}
    Let \( \mathbb P \) be a forcing poset.
    The \emph{\( \mathbb P \)-forcing language} \( \mathcal{FL}_{\mathbb P} \) is the class of logical formulas formed using the binary relation \( \in \) and constant symbols from \( \mathrm{V}^{\mathbb P} \).
\end{definition}
\begin{definition}
    Let \( \mathbb P \) be a forcing poset and let \( p \in \mathbb P \).
    Let \( \dot x, \dot y, \dot u \) be \( \mathbb P \)-names in \( \mathrm{V} \).
    We define the \emph{forcing relation} \( p \Vdash \varphi(\dot u) \) recursively as follows.
    \begin{enumerate}
        \item \( p \Vdash \varphi(\dot u) \wedge \psi(\dot u) \) if and only if \( p \Vdash \varphi(\dot u) \) and \( p \Vdash \psi(\dot u) \);
        \item \( p \Vdash \neg\varphi(\dot u) \) if and only if there is no \( q \leq p \) such that \( q \Vdash \varphi(\dot u) \);
        \item \( p \Vdash \exists x.\, \varphi(x, \dot u) \) if and only if the set
        \[ \qty{q \leq p \mid \exists \dot x \in \mathrm{V}^{\mathbb P}.\, q \Vdash \varphi(\dot x, \dot u)} \]
        is dense below \( p \);
        \item \( p \Vdash \dot x \in \dot y \) if and only if the set
        \[ \qty{q \leq p \mid \exists \langle r, \dot z \rangle \in \dot y.\, q \leq r \wedge (q \Vdash \dot x = \dot z)} \]
        is dense below \( p \);
        \item \( p \Vdash \dot x \subseteq \dot y \) if and only if for all \( \langle q_1, \dot z_1 \rangle \in \dot x \), the set
        \[ \qty{r \leq p \mid r \leq q_1 \to \exists \langle q_2, \dot z_2 \rangle \in \dot y.\, r \leq q_2 \wedge (r \Vdash \dot z_1 = \dot z_2)} \]
        is dense below \( p \); and
        \item \( p \Vdash \dot x = \dot y \) if and only if \( p \Vdash \dot x \subseteq \dot y \) and \( p \Vdash \dot y \subseteq \dot x \).
    \end{enumerate}
\end{definition}
\begin{remark}
    \begin{enumerate}
        \item The definitions for \( \subseteq \) and \( = \) are defined recursively, and thus require transfinite recursion to define formally.
        \item All of the clauses except for the existential use only absolute notions.
        In particular, it does not depend on \( M \).
        When relativising to a model, \( (p \Vdash \exists x.\, \varphi(x))^M \) precisely when the set
        \[ \qty{q \leq p \mid \exists \dot x \in M^{\mathbb P}.\, q \Vdash \varphi(\dot x, \dot u)} \]
        is dense below \( p \).
    \end{enumerate}
\end{remark}
\begin{proposition}
    Let \( p \) be a condition, \( \varphi \) be an \( \mathcal{FL}_{\mathbb P} \)-formula, and \( \dot x_1, \dots, \dot x_n \) be \( \mathbb P \)-names in \( \mathrm{V} \).
    Then the following are equivalent.
    \begin{enumerate}
        \item \( p \Vdash \varphi(\dot x_1, \dots, \dot x_n) \);
        \item for all \( q \leq p \), \( q \Vdash \varphi(\dot x_1, \dots, \dot x_n) \);
        \item there is no \( q \leq p \) such that \( q \Vdash \neg\varphi(\dot x_1, \dots, \dot x_n) \);
        \item the set \( \qty{r \mid r \Vdash \varphi(\dot x_1, \dots, \dot x_n)} \) is dense below \( p \).
    \end{enumerate}
\end{proposition}
\begin{proof}
    \emph{(ii) implies (iii).}
    If (iii) did not hold, there would be some \( q \leq p \) such that \( q \Vdash \neg\varphi \).
    Then there is no \( r \leq q \) such that \( r \Vdash \varphi \).
    So in particular, \( q \nVdash \varphi \), contradicting (ii).

    \emph{(iii) implies (iv).}
    Suppose that there is no \( q \leq p \) such that \( q \Vdash \neg\varphi \).
    Take \( q \leq p \).
    Then by assumption, \( q \nVdash \neg\varphi \), so there is \( r \leq q \) such that \( r \Vdash \varphi \), so the set is dense as required.

    \emph{(i) implies (ii).}
    We show this by induction on formula complexity.
    \begin{itemize}
        \item For atomic formulas, let \( \mdwhtsquare \) be either \( \in \) or \( \subseteq \).
        Then \( p \Vdash \dot x \mathrel{\mdwhtsquare} \dot y \) if and only if some set \( A \) is dense below \( p \).
        Take \( q \leq p \), then \( A \) is dense below \( q \).
        Then \( q \Vdash \dot x \mathrel{\mdwhtsquare} \dot y \) as required.
        \item If \( p \Vdash \neg\varphi \), then there is no \( r \leq p \) such that \( r \Vdash \varphi \).
        Then there is no \( r \leq q \) such that \( r \Vdash \varphi \), so by definition, \( q \Vdash \neg\varphi \).
        \item If \( p \Vdash \varphi \wedge \psi \) then \( p \Vdash \varphi \) and \( p \Vdash \psi \), so by the inductive hypothesis, \( q \Vdash \varphi \) and \( q \Vdash \psi \), giving \( q \Vdash \varphi \wedge \psi \).
        \item If \( p \Vdash \exists x.\, \varphi(x) \), then \( A \) is dense below \( p \) for some set \( A \), but then \( A \) is dense below \( q \), so \( q \Vdash \exists x.\, \varphi(x) \).
    \end{itemize}

    \emph{(iv) implies (i).}
    Again, we show this by induction.
    \begin{itemize}
        \item For atomic formulas, let \( \mdwhtsquare \) be either \( \in \) or \( \subseteq \).
        To prove that \( p \Vdash \dot x \mathrel{\mdwhtsquare} \dot y \), we must show that some set \( A \) is dense below \( p \).
        By assumption, the set \( \qty{r \mid r \Vdash \dot x \mathrel{\mdwhtsquare} \dot y} \) is dense below \( p \).
        Fix \( q \leq p \), then there is \( r \leq q \) such that \( r \Vdash \dot x \mathrel{\mdwhtsquare} \dot y \).
        Hence there is some \( s \leq r \leq q \leq p \) such that \( s \in A \).
        Therefore \( p \Vdash \dot x \mathrel{\mdwhtsquare} \dot y \) as required.
        The proof for existentials is the same.
        \item Suppose that \( \qty{r \mid r \Vdash \varphi \wedge \psi} \) is dense below \( p \).
        So \( \qty{r \mid r \Vdash \varphi} \) and \( \qty{r \mid r \Vdash \psi} \) are also dense below \( p \).
        By the inductive hypothesis, \( p \Vdash \varphi \) and \( p \Vdash \psi \).
        Hence \( p \Vdash \varphi \wedge \psi \).
        \item Suppose that \( \qty{r \mid r \Vdash \neg\varphi} \) is dense below \( p \).
        To show \( p \Vdash \neg\varphi \), we fix \( q \leq p \) and suppose \( q \Vdash \varphi \).
        By the fact that (i) implies (iii), there is no \( r \leq q \) such that \( r \Vdash \neg\varphi \), contradicting density of the set \( \qty{r \mid r \Vdash \neg\varphi} \).
    \end{itemize}
\end{proof}
\begin{proposition}
    Let \( \mathbb P \) be a forcing poset, let \( p, q \in \mathbb P \), and let \( \dot a, \dot b \in \mathrm{V}^{\mathbb P} \).
    Then
    \begin{enumerate}
        \item \( p \Vdash \dot a = \dot a \);
        \item if \( \langle q, \dot b \rangle \in \dot a \) and \( p \leq q \), then \( p \Vdash \dot b \in \dot a \);
        \item if \( M \) is a transitive model of \( \mathsf{ZF} \) and \( \mathbb P \in M \), then for any \( \varphi, \psi \),
        \[ \qty{\langle q, \dot x \rangle \mid \langle q, \dot x \rangle \in \dot a \wedge (q \Vdash \varphi(\dot x))^M} \in M \]
        and
        \[ \qty{q \in \mathbb P \mid q \Vdash (\psi(\dot a))^{\check M}} \in M \]
        \item \( p \Vdash \varphi \vee \psi \) if and only if
        \[ \qty{q \leq p \mid q \Vdash \varphi \text{ or } q \Vdash \psi} \]
        is dense below \( p \);
        \item \( p \Vdash \varphi \to \psi \) if and only if there is no \( q \leq p \) such that \( q \Vdash \varphi \) and \( q \Vdash \neg \psi \);
        \item \( p \Vdash \forall x.\, \varphi(x) \) if and only if for all \( \dot x \in \mathrm{V}^{\mathbb P} \), \( p \Vdash \varphi(\dot x) \);
        \item for any \( \varphi \), the set
        \[ \qty{p \in \mathbb P \mid p \Vdash \varphi \text{ or } p \Vdash \neg\varphi} \]
        is a dense open set;
        \item there is no \( p \) and formula \( \varphi \) such that
        \[ p \Vdash \varphi \wedge \neg\varphi \]
    \end{enumerate}
\end{proposition}

\subsection{The forcing theorem}
\begin{theorem}[the forcing theorem]
    Suppose \( M \) be a transitive model of \( \mathsf{ZF} \), \( \mathbb P \in M \) is a forcing poset, \( \varphi(u) \) is a formula, and \( G \) is \( \mathbb P \)-generic over \( M \).
    Then for any \( \dot x \in M^{\mathbb P} \),
    \begin{enumerate}
        \item if \( p \in G \) and \( (p \Vdash \varphi(x))^M \), then \( M[G] \vDash \varphi(\dot x^G) \); and
        \item if \( M[G] \vDash \varphi(\dot x^G) \), then there is a condition \( p \in G \) such that \( (p \Vdash \varphi(x))^M \).
    \end{enumerate}
\end{theorem}
Once we have shown this theorem, we will have the following result.
\begin{corollary}
    Suppose that \( M \) is a countable transitive model of \( \mathsf{ZF} \), \( \mathbb P \in M \) is a forcing poset, and \( \varphi(u) \) is a formula.
    Then for any name \( \dot x \in M^{\mathbb P} \),
    \[ (p \Vdash \varphi(\dot x))^m \leftrightarrow \text{for any \( \mathbb P \)-generic filter \( G \) with \( p \in G \), } M[G] \Vdash \varphi(\dot x)^G \]
\end{corollary}
The only reason we need countability is so that every condition is contained in a generic filter.
\begin{proof}
    The forward direction is part (i) of the forcing theorem.
    For the backward direction, suppose that \( (p \nVdash \varphi(\dot x))^M \).
    Then, by definition, there is some \( q \leq p \) such that \( (q \Vdash \neg\varphi(\dot x))^M \).
    Let \( G \) be a \( \mathbb P \)-generic filter over \( M \) such that \( q \in G \).
    Then, since \( G \) is upwards closed, \( p \in G \).
    Hence \( M[G] \vDash \varphi(\dot x^G) \) by assumption.
    But as \( q \in G \), by the forcing theorem we obtain \( M[G] \vDash \neg\varphi(\dot x^G) \).
    This contradicts part (viii) of the proposition above by the forcing theorem.
\end{proof}
\begin{definition}
    Suppose \( M \) is a countable transitive model of \( \mathsf{ZF} \), \( \mathbb P \in M \) is a forcing poset, \( \dot x_1, \dots, \dot x_n \in M^{\mathbb P} \), \( p \in \mathbb P \), and \( \varphi(v_1, \dots, v_n) \) is a formula.
    Then we can define a relation \( \Vdash^\star_{\mathbb P, M} \) by
    \[ p \Vdash^\star_{\mathbb P, M} \varphi(\dot x_1, \dots, \dot x_n) \]
    if and only if \( M[G] \vDash \varphi(\dot x_1^G, \dots, \dot x_n^G) \) for all \( G \subseteq \mathbb P \) such that \( p \in G \) and \( G \) is a \( \mathbb P \)-generic filter.
\end{definition}
\begin{corollary}
    \( p \Vdash \varphi \leftrightarrow p \Vdash^\star_{\mathbb P, M} \varphi \).
\end{corollary}
We will now prove the forcing theorem.
\begin{proof}
    We show the result by induction on the complexity of formulas.
    Note that we need to work with relativised formulas with parameters \( (p \Vdash \varphi(\vb v))^M \), but this only changes the existential case, so for all other cases we will suppress the relativisation and the parameters.
    We write \( \Psi(\varphi) \) for the claim that for any name \( \dot x \in M^{\mathbb P} \), if \( p \in G \) and \( (p \Vdash \varphi(\dot x))^M \), then \( M[G] \vDash \varphi(\dot x^G) \), and if \( M[G] \vDash \varphi(\dot x)^G \), then there exists \( p \in G \) such that \( (p \Vdash \varphi(\dot x))^M \).

    \emph{Part (i): negations.}
    Suppose \( \Psi(\varphi) \) holds.
    Let \( p \in G \) and \( p \Vdash \neg \varphi \).
    Suppose for a contradiction that \( M[G] \vDash \varphi \), or equivalently, \( \varphi^{M[G]} \).
    Then as \( \Psi(\varphi) \) holds, there is \( q \in G \) such that \( q \Vdash \varphi \).
    As \( G \) is a filter, there is \( r \in G \) such that \( r \leq p, q \).
    Then \( r \Vdash \varphi \), which contradicts the definition of \( p \Vdash \neg\varphi \).
    Hence \( \neg(\varphi^{M[G]}) \), so by definition \( (\neg \varphi)^{M[G]} \), so \( M[G] \vDash \neg\varphi \).

    For the converse, suppose \( M[G] \vDash \neg\varphi \).
    Let
    \[ D = \qty{p \in \mathbb P \mid p \Vdash \varphi \vee p \Vdash \neg\varphi} \]
    Then \( D \) is dense, because if \( q \nVdash \varphi \), then there is \( p \leq q \) such that \( p \Vdash \neg\varphi \), and \( p \in D \).
    So as \( G \) is generic, we can fix \( p \in G \cap D \).
    If \( p \Vdash \varphi \), then by \( \Psi(\varphi) \) we must have \( M[G] \vDash \varphi \), but we assumed \( M[G] \vDash \neg\varphi \).
    Hence \( p \Vdash \neg\varphi \).

    \emph{Part (ii): conjunctions.}
    Suppose \( \Psi(\varphi) \) and \( \Psi(\psi) \).
    Suppose \( p \Vdash \varphi \wedge \psi \) for some \( p \in G \), so by definition, \( p \Vdash \varphi \) and \( p \Vdash \psi \).
    By \( \Psi(\varphi) \) and \( \Psi(\psi) \), we have \( M[G] \vDash \varphi \) and \( M[G] \vDash \psi \).
    So \( M[G] \vDash \varphi \wedge \psi \).

    For the converse, suppose \( M[G] \vDash \varphi \wedge \psi \).
    Then \( M[G] \vDash \varphi \) and \( M[G] \vDash \psi \), so there are \( p, q \in G \) such that \( p \Vdash \varphi \) and \( q \Vdash \psi \).
    But \( G \) is a filter, so there is \( r \leq p, q \) such that \( r \Vdash \varphi \) and \( r \Vdash \psi \).
    Hence \( r \Vdash \varphi \wedge \psi \), as required.

    \emph{Part (iii): existential quantifiers.}
    For this case, we will not suppress relativisation and parameters.
    Suppose \( \Psi(\varphi(\dot x)) \); we show \( \Psi(\exists x.\, \varphi(x)) \).
    To be more precise, for all names \( \dot x \in M^{\mathbb P} \), we assume the forcing theorem holds for \( \varphi(\dot x) \).
    Suppose \( p \in G \) is such that \( (p \Vdash \exists x.\, \varphi(x))^M \).
    Let
    \[ D = \qty(\qty{q \leq p \mid \exists \dot x \in \mathrm{V}^{\mathbb P}.\, (q \Vdash \varphi(\dot x))})^M = \qty{q \leq p \mid \exists \dot x \in M^{\mathbb P}.\, (q \Vdash \varphi(\dot x))^M} \in M \]
    By definition of forcing existentials, \( D \) is a dense set.
    Since \( G \) is generic, there is some \( q \in G \cap D \).
    Then we can fix some \( \mathbb P \)-name \( \dot x \) such that \( (q \Vdash \varphi(\dot x))^M \).
    Since the forcing theorem holds for \( \varphi(\dot x) \), we have \( M[G] \vDash \varphi(\dot x^G) \).
    Hence \( M[G] \vDash \exists x.\, \varphi(x) \).

    Now suppose \( M[G] \vDash \exists x.\, \varphi(x) \).
    We can fix \( \dot x \in M^{\mathbb P} \) such that \( M[G] \vDash \varphi(\dot x^G) \).
    By the fact that \( \Psi(\varphi(\dot x)) \) holds, there is a condition \( p \) such that \( (p \Vdash \varphi(\dot x))^M \).
    Then
    \[ \qty{q \leq p \mid (q \Vdash \varphi(\dot x))^M} \]
    is dense.
    Hence, by definition, \( (p \vDash \exists x.\, \varphi(x))^M \).

    \emph{Part (iv): equality.}
    Recall that \( p \Vdash \dot x = \dot y \) if and only if
    \begin{enumerate}[(a)]
        \item for all \( \langle q_1, \dot z_1 \rangle \in \dot x \), \( \qty{r \leq p \mid r \leq q_1 \to \exists \langle q_2, \dot z_2 \rangle \in \dot y.\, r \leq q_2 \wedge (r \Vdash \dot z_1 = \dot z_2)} \) is dense below \( p \); and
        \item for all \( \langle q_2, \dot z_2 \rangle \in \dot y \), \( \qty{r \leq p \mid r \leq q_2 \to \exists \langle q_1, \dot z_1 \rangle \in \dot x.\, r \leq q_1 \wedge (r \Vdash \dot z_1 = \dot z_2)} \) is dense below \( p \).
    \end{enumerate}
    We show that for any \( \dot x, \dot y \), we have \( \Psi(\dot x = \dot y) \).
    We will show this by transfinite induction on the pair \( \langle \dot x, \dot y \rangle \) ordered lexicographically.

    Suppose that \( p \Vdash \dot x = \dot y \) and \( p \in G \).
    We show \( M[G] \vDash \dot x^G \subseteq \dot y^G \); the converse holds by symmetry, and then we obtain \( M[G] \vDash \dot x^G = \dot y^G \) by extensionality.
    Any element of \( \dot x^G \) is of the form \( \dot z_1^G \) where \( \langle q_1, \dot z_1 \rangle \in \dot x \) and \( q_1 \in G \).
    Since \( G \) is a filter, we can fix \( s \in G \) such that \( s \leq p, q_1 \).
    Then, as \( s \leq p \), we have \( s \Vdash \dot x = \dot y \), so the set in (a) above is dense below \( s \).
    Hence there is \( r \in G \) such that \( r \leq s \leq q_1 \) and there exists \( \langle q_2, \dot z_2 \rangle \in \dot y \) such that \( r \leq q_2 \) and \( r \Vdash \dot z_1 = \dot z_2 \).
    As \( G \) is a filter, \( q_2 \in G \), so \( \dot z_2^G \in \dot y^G \).
    By using the inductive hypothesis on \( \langle \dot z_1, \dot z_2 \rangle \), as \( r \in G \) we have \( M[G] \vDash \dot z_1^G = \dot x_2^G \).
    Hence \( \dot z_1^G \in \dot y^G \), so \( \dot x^G \subseteq \dot y^G \).

    For the converse, \( M[G] \vDash \dot x^G = \dot y^G \).
    Define \( D \) to be the set of \( r \in \mathbb P \) such that at least one of the following hold.
    \begin{enumerate}
        \item[(0)] \( r \Vdash \dot x = \dot y \);
        \item[(a\( ' \))] there exists \( \langle q_1, \dot z_1 \rangle \in \dot x \) such that \( r \leq q_1 \) and for all \( \langle q_2, \dot z_2 \rangle \in \dot y \) and \( s \in \mathbb P \), if \( s \leq q_2 \) and \( s \Vdash \dot z_1 = \dot z_2 \) then \( s \perp r \);
        \item[(b\( ' \))] there exists \( \langle q_2, \dot z_2 \rangle \in \dot y \) such that \( r \leq q_2 \) and for all \( \langle q_1, \dot z_1 \rangle \in \dot x \) and \( s \in \mathbb P \), if \( s \leq q_1 \) and \( s \Vdash \dot z_1 = \dot z_2 \) then \( s \perp r \).
    \end{enumerate}
    Note that by separation in \( M \) and absoluteness, \( D \) is a set in \( M \).
    We claim that \( D \) is dense.
    Fix \( p \in \mathbb P \), and suppose \( p \nVdash \dot x = \dot y \).
    Then at least one of (a) and (b) above fails.
    Suppose that the set in (a) fails; the result for (b) holds by symmetry.
    Then there is \( \langle q_1, \dot z_1 \rangle \in \dot x \) such that
    \[ \qty{r \leq p \mid r \leq q_1 \to \exists \langle q_2, \dot z_2 \rangle \in \dot y.\, r \leq q_2 \wedge (r \Vdash \dot z_1 = \dot z_2)} \]
    is not dense below \( p \).
    Then there is \( s \leq p \) such that for all \( r \leq s \), we have \( r \leq q_1 \), and for all \( \langle q_2, \dot z_2 \rangle \in \dot y \) such that \( \neg((r \Vdash \dot z_1 = \dot z_2) \wedge r \leq q_2) \).
    In particular, this gives \( s \leq q_1 \).
    Now, if \( \langle q_1, \dot z_2 \rangle \in \dot y \), \( r \leq q_2 \), and \( r \Vdash \dot z_1 = \dot z_2 \), then it must be the case that \( s \perp r \), as any common extension of \( s \) and \( r \) would contradict the fact that the set in (a) was not dense.
    Thus \( s \leq p \) and \( s \) satisfies (a\( ' \)).
    Hence \( D \) is dense.

    \( D \) is dense below \( p \in G \) and \( G \) is \( \mathbb P \)-generic so we can fix \( r \in G \cap D \).
    We will show that \( r \) satisfies (0), which finishes the proof.
    Suppose not, so suppose \( r \) satisfies (a\( ' \)) without loss of generality.
    Then we can fix \( \langle q_1, \dot z_1 \rangle \in \dot x \) such that \( r \leq q_1 \) and for all \( \langle q_2, \dot z_2 \rangle \in \dot y \) such that for all \( s \in \mathbb P \) with \( s \leq q_2 \) and \( s \Vdash \dot z_1 = \dot z_2 \), we have \( s \perp r \).
    Since \( r \in G \) and \( r \leq q_1 \), we must have \( q_1 \in G \) by upwards closure.
    Therefore, \( M[G] \vDash \dot z_1^G \in \dot x^G = \dot y^G \).
    So we can fix \( \langle q_2, \dot z_2 \rangle \in \dot y \) such that \( q_2 \in G \) and \( M[G] \vDash \dot z_1^G = \dot z_2^G \).
    By the inductive hypothesis, we can fix \( p' \in G \) such that \( p' \Vdash \dot z_1 = \dot z_2 \).
    Since \( G \) is a filter and both \( p', q_2 \in G \), we obtain \( s \in G \) with \( s \leq p', q_2 \).
    Hence \( s \Vdash \dot z_1 = \dot z_2 \).
    Hence, by (a\( ' \)), we have \( s \perp r \).
    But \( s, r \in G \), so \( s \mathrel\| r \), giving a contradiction.

    \emph{Part (v): membership.}
    Suppose that \( p \Vdash \dot x \in \dot y \) for \( p \in G \).
    Let
    \[ D = \qty{q \leq p \mid \exists \langle r, \dot z \rangle \in \dot y.\, q \leq r \wedge (q \Vdash \dot x = \dot z)} \]
    By definition, \( D \) is dense.
    We can fix \( q \in G \cap D \).
    Since \( q \in D \), we may also fix \( \langle r, \dot z \rangle \in \dot y \) such that \( q \leq r \) and \( q \Vdash \dot x = \dot z \).
    As \( q \in G \), by the forcing theorem for equality, \( M[G] \vDash \dot x^G = \dot z^G \).
    Since \( G \) is a filter and \( q \leq r \), then \( r \in G \) and so \( \dot z^G \in \dot y^G \).
    Hence \( M[G] \vDash \dot x^G \in \dot y^G \).

    Now suppose \( M[G] \vDash \dot x^G \in \dot y^G \).
    Fix \( \langle r, \dot z \rangle \in \dot y \) such that \( r \in G \) and \( \dot z^G = \dot x^G \).
    Now, by the forcing theorem for equality, there is \( q \in G \) such that \( q \Vdash \dot x = \dot z \).
    Since \( G \) is a filter and \( q, r \in G \), we can fix \( p \in G \) such that \( p \leq q, r \).
    Then \( p \Vdash \dot z \in \dot y \) and \( p \Vdash \dot x = \dot z \).
    So for all \( s \leq p \), we have \( s \leq r \) and \( s \Vdash \dot x = \dot z \), so \( D \) is dense below \( p \).
    Hence \( p \Vdash \dot x \in \dot y \), as required.
\end{proof}

\subsection{\texorpdfstring{\( \mathsf{ZF} \)}{ZF} in forcing extensions}
\begin{lemma}
    Suppose that \( M \) is a countable transitive model of \( \mathsf{ZF} \), \( \mathbb P \in M \) is a forcing poset, and \( G \subseteq \mathbb P \) is a generic filter.
    Then \( M[G] \) models separation.
\end{lemma}
\begin{proof}
    Let \( \varphi(x, v) \) be a formula with free variables \( x, v \).
    It suffices to show that for any \( a, v \in M[G] \),
    \[ b = \qty{x \in a \mid M[G] \vDash \varphi(x, v)} \in M[G] \]
    Fix names \( \dot a, \dot v \) such that \( \dot a^G = a \) and \( \dot v^G = v \).
    Any member of \( \dot a^G \) is of the form \( \dot x^G \) where \( \langle p, \dot x \rangle \in \dot a \) and \( p \in G \).
    Then
    \[ b = \qty{\dot x^G \mid \exists p \in G.\, \langle p, \dot x \rangle \in \dot a \wedge M[G] \vDash \varphi(\dot x^G, \dot v^G)} \]
    We define
    \[ \dot b = \qty{\langle p, \dot x \rangle \mid \langle p, \dot x \rangle \in \dot a \wedge (p \Vdash \varphi(\dot x, \dot v))^M} \in M^{\mathbb P} \]
    Thus, \( \dot b^G \in M[G] \), so it suffices to show \( \dot b^G = b \).
    We have \( x \in \dot b^G \) if and only if there is some \( \mathbb P \)-name \( \dot x \) in \( M \) and \( p \in G \) such that \( \dot x^G = x \), \( \langle p, \dot x \rangle \in \dot a \), and \( (p \Vdash \varphi(\dot x, \dot v))^M \).
    By the forcing theorem, this is equivalent to the statement \( x \in \dot a^G \) and \( M[G] \vDash \varphi(x, v) \), which is precisely the statement \( x \in b \).
\end{proof}
The arguments for collection and power set will follow the same pattern.
\begin{lemma}
    Suppose that \( M \) is a countable transitive model of \( \mathsf{ZF} \), \( \mathbb P \in M \) is a forcing poset, and \( G \subseteq \mathbb P \) is a generic filter.
    Then \( M[G] \) models collection.
\end{lemma}
\begin{proof}
    Let \( \varphi(x, y, v) \) be a formula with free variables \( x, y, v \).
    Fix \( a, v \in M[G] \) with names \( \dot a, \dot v \).
    Suppose \( M[G] \vDash \forall x \in a.\, \exists y.\, \varphi(x, y, v) \).
    We claim that there is \( b \in M[G] \) such that \( M[G] \vDash \forall x \in a.\, \exists y \in b.\, \varphi(x, y, v) \).
    Let
    \[ C = \qty{\langle p, \dot x \rangle \mid p \in \mathbb P \wedge x \in \ran a \wedge \exists \dot y \in M^{\mathbb P}.\, (p \Vdash \varphi(\dot x, \dot y, \dot v))^M} \]
    Then for all \( \langle p, \dot x \rangle \in C \), there is \( \dot y \in M^{\mathbb P} \) such that \( (p \Vdash \varphi(\dot x, \dot y, \dot v))^M \).
    Note that the collection of such \( \dot y \) might not form a set, for example with the formula \( \varphi(x, y) \equiv x \in y \).
    However, using collection in \( M \), we may form a set \( B \in M \) such that \( B \subseteq M^{\mathbb P} \) and
    \[ \forall \langle p, x \rangle \in C.\, \exists \dot y \in B.\, (p \Vdash \varphi(\dot x, \dot y, \dot v))^M \]
    Finally, set
    \[ \dot b = \qty{\langle \Bbbone, \dot y \rangle \mid \dot y \in B} \in M^{\mathbb P} \]
    We show that \( b = \dot b^G \) satisfies the required property.
    Fix some \( x \in a \), then by definition there is \( \langle q, \dot x \rangle \in \dot a \) such that \( q \in G \) and \( \dot x^G = x \).
    By assumption, \( M[G] \vDash \exists y \in b.\, \varphi(x, y, v) \).
    So fix \( \dot z^G \) such that \( M[G] \vDash \varphi(x, z, v) \).
    By the forcing theorem, there is \( p \in G \) such that \( (p \Vdash \varphi(\dot x, \dot z, \dot v))^M \).
    Hence \( \langle p, \dot x \rangle \in C \).
    So we can fix \( \dot y \in B \) such that \( (p \Vdash \varphi(\dot x, \dot y, \dot v))^M \).
    Therefore, \( \langle \Bbbone 1, \dot y \rangle \in \dot b \).
    Since \( \Bbbone 1 \in G \), \( \dot y^G \in \dot b^G \).
    By the forcing theorem again,
    \[ M[G] \vDash \dot y^G \in \dot b^G \wedge \varphi(\dot x^G, \dot y^G, v) \]
    Hence, collection holds.
\end{proof}
Note that since power set has not been used in any of the previous proofs, if \( M \vDash \mathsf{ZF}^- \), then \( M[G] \vDash \mathsf{ZF}^- \).
\begin{lemma}
    Suppose that \( M \) is a countable transitive model of \( \mathsf{ZF} \), \( \mathbb P \in M \) is a forcing poset, and \( G \subseteq \mathbb P \) is a generic filter.
    Then \( M[G] \) models the axiom of power set.
\end{lemma}
\begin{proof}
    By separation, it suffices to show that if \( a \in M[G] \), then
    \[ \mathcal P(a) \cap M[G] = \qty{x \in M[G] \mid x \subseteq a} \subseteq b \]
    for some set \( b \in M[G] \).
    Fix \( a \in M[G] \) with name \( \dot x \in M^{\mathbb P} \), and define
    \[ S = \qty{\dot x \in M^{\mathbb P} \mid \ran \dot x \subseteq \ran \dot a} = \mathcal P(\mathbb P \times \ran \dot a)^M \]
    and let
    \[ \dot b = \qty{\langle \Bbbone, \dot x \rangle \mid x \in S} \in M^{\mathbb P} \]
    Let \( c \in \mathcal P(a) \cap M[G] \); we must show that \( c \in \dot b^G \).
    Let \( \dot c \in M^{\mathbb P} \) be a name for \( c \), and let
    \[ \dot x = \qty{\langle p, \dot z \rangle \mid \dot z \in \ran \dot a \wedge (p \Vdash \dot z \in \dot c)^M} \in S \]
    We claim \( \dot x^G = \dot c^G = c \).
    First, we show \( \dot x^G \subseteq c \).
    Fix \( \dot z^G \in \dot x^G \).
    By definition, we can fix \( p \in G \) such that \( \langle p, \dot z \rangle \in \dot x \).
    From this, it follows that \( \dot z \in \ran \dot a \) and \( p \Vdash \dot z \in \dot c \).
    Since \( p \in G \), by the forcing theorem, \( M[G] \vDash \dot z^G \in \dot c^G \), as required.

    Conversely, since \( M[G] \vDash c \subseteq \dot a^G \), so every element of \( c \) is of the form \( \dot z^G \) for \( \langle q, \dot z \rangle \in \dot a \) with \( q \in G \).
    Also, if \( M[G] \vDash \dot z^G \in c \), then by the forcing theorem, there is \( p \) such that \( p \Vdash \dot z \in \dot c \).
    Then \( \langle p, \dot z \rangle \in \dot x \), so \( \dot z^G \in \dot x^G \).
\end{proof}
\begin{lemma}
    Suppose that \( M \) is a countable transitive model of \( \mathsf{ZFC}^- \), \( \mathbb P \in M \) is a forcing poset, and \( G \subseteq \mathbb P \) is a generic filter.
    Then \( M[G] \) models the well-ordering principle, and hence models \( \mathsf{ZFC}^- \).
\end{lemma}
\begin{proof}
    It suffices to show that any \( a \in M[G] \) can be well-ordered in \( M[G] \).
    Fix a name \( \dot a \) for \( a \).
    Using the well-ordering principle in \( M \), we can enumerate the elements of \( \ran \dot a \) as
    \[ \qty{\dot x_\alpha \mid \alpha < \delta} \]
    Let
    \[ \dot f = \qty{\langle \Bbbone, \operatorname{op}(\check \alpha, \dot x_\alpha) \rangle \mid \alpha < \delta} \in M^{\mathbb P} \]
    So in \( M[G] \),
    \[ \dot f^G = \qty{\langle \alpha, \dot x_\alpha^G \rangle \mid \alpha < \delta} \]
    Hence \( \dot f^G \) is a function with domain \( \delta \), and \( a \subseteq \ran \dot f^G \).
    We can now define a well-order \( \triangleleft \) on \( a \) by defining that \( x \triangleleft y \) if and only if
    \[ \min\qty{\alpha < \delta \mid \dot f^G(\alpha) = x} < \min\qty{\alpha < \delta \mid \dot f^G(\alpha) = y} \]
\end{proof}
\begin{remark}
    \begin{enumerate}
        \item \( \dot f^G \) may not be injective, since we could have \( \dot x_\alpha^G = \dot x_\beta^G \) for \( \alpha \neq \beta \).
        \item \( \ran \dot f^G \) may not equal \( a \).
        Elements of \( \dot a \) are conditions \( \langle p, \dot x_\alpha \rangle \), and if \( p \notin G \), we may not have \( \dot x_\alpha^G \in a \).
        \item For power set, it sufficed to find a set of names which contained enough names to represent all possible subsets of \( a \).
        However, there are a proper class of names for the empty set, so we could not produce a set of all such names.
        \item The statement \( M[G] \vDash \varphi \) should be considered a ternary relation between \( M \), \( G \), and \( \varphi \).
        It is possible that \( G \) and \( H \) are both generic, but \( M[G] \vDash \varphi \) and \( M[H] \vDash \neg\varphi \).
        \item The relativisation \( (p \Vdash \varphi)^M \) will be dropped when clear in subsequent sections.
    \end{enumerate}
\end{remark}
\begin{lemma}
    Let \( M \) be a countable transitive model of \( \mathsf{ZFC} \) and let \( \mathbb P \in M \) be a forcing poset.
    Let \( \varphi, \psi \) be \( \mathcal{FL}_{\mathbb P} \)-formulas.
    Then, for any \( p \in \mathbb P \) and \( \dot x \in M^{\mathbb P} \),
    \begin{enumerate}
        \item if \( \mathsf{ZFC} \vdash \forall v.\, \varphi(v) \to \psi(v) \) then \( (p \Vdash \varphi(\dot x))^M \to (p \Vdash \psi(\dot x))^M \); and
        \item if \( \mathsf{ZFC} \vdash \forall v.\, \varphi(v) \leftrightarrow \psi(v) \) then \( (p \Vdash \varphi(\dot x))^M \leftrightarrow (p \Vdash \psi(\dot x))^M \).
    \end{enumerate}
\end{lemma}
Informally, forcing is closed under logical equivalence.
\begin{proof}
    Clearly (ii) follows from (i).
    Suppose that \( \mathsf{ZFC} \vdash \forall v.\, \varphi(v) \to \psi(v) \) and \( (p \Vdash \varphi(\dot x))^M \).
    Since \( M \) is countable, we can let \( G \) be a \( \mathbb P \)-generic filter over \( M \) such that \( p \in G \).
    By the forcing theorem, \( M[G] \vDash \varphi(\dot x^G) \).
    Since \( M[G] \vDash \mathsf{ZFC} \), we have \( M[G] \vDash \psi(\dot x^G) \).
    Hence, by the forcing theorem in the reverse direction, as this is true for all generics containing \( p \) we have \( (p \Vdash \psi(\dot x))^M \).
\end{proof}
